package minsat;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.Set;

/**
 * Represents an overall formula that makes up a MinSat instance. Consists of a list of Clauses
 */
public class Formula
{
  private List<Clause> clauses;

  public Formula()
  {
    clauses = new ArrayList<Clause>();
  }

  public Formula(Formula formula)
  {
    this();
    for (Clause c : formula.clauses)
      this.clauses.add(new Clause(c));
  }

  public void addClause(String literals, Double weight)
  {
    clauses.add(new Clause(literals, weight));
  }

  public void addClause(String literals, int weight)
  {
    clauses.add(new Clause(literals, new Double(weight)));
  }

  public void addClause(Clause clause)
  {
    clauses.add(clause);
  }

  public String toString()
  {
    String result = "";
    for (Clause c : clauses) {
      result += c + " ";
    }
    return result;
  }

  public final List<Clause> getClauses()
  {
    return clauses;
  }

  /**
   * @return Combined weights of empty soft clauses in this formula
   */
  public double empty()
  {
    double ret = 0;

    for (Clause c : clauses) {
      if (!c.isHard() && c.literals.isEmpty()) ret += c.weight;
    }

    return ret;
  }

  /**
   * @return True if the formula is empty or all of its clauses are empty
   */
  public boolean isEmpty()
  {
    if (clauses.isEmpty())
      return true;
    else
      for (Clause c : clauses)
        if (!c.literals.isEmpty()) return false;

    return true;
  }

  /**
   * Given a new literal binding L, perform unit propagation by satisfying clauses containing L and
   * removing occurrences of !L
   * 
   * @param newBinding
   *          The new binding, null when the program starts
   * @param failOnEmptySoftClause
   *          Empty hard clauses always cause errors; if true, empty soft clauses do as well (used
   *          to propagate soft clauses during graph building)
   */
  public void propagate(Binding newBinding, BindingsAndBound bindings, boolean failOnEmptySoftClause)
      throws IllegalEmptyClauseException
  {
    boolean removed;
    Clause clause;
    Literal literal;
    List<Binding> generatedBindings = new ArrayList<Binding>();

    // if this is the first call we need to check for duplicate literals or tautologies
    if (newBinding == null) {
      Set<Literal> literalsInClause;

      // apply to every clause in this formula
      Iterator<Clause> clauseItr = clauses.iterator();
      while (clauseItr.hasNext()) {
        literalsInClause = new HashSet<Literal>();
        clause = clauseItr.next();
        removed = false;

        // apply to clause by checking binding against each literal in clause
        Iterator<Literal> literalItr = clause.literals.iterator();
        while (literalItr.hasNext() && !removed) {
          literal = literalItr.next();

          // this is a duplicate, so remove it
          if (literalsInClause.contains(literal)) {
            literalItr.remove();
            continue;
          }
          // tautology, so remove the clause
          else if (literalsInClause.contains(literal.opposite())) {
            clauseItr.remove();
            removed = true;
            continue;
          }

          literalsInClause.add(literal);
        }

        // we can propagate this
        if (clause.isHard() && clause.literals.size() == 1) {
          if (newBinding == null)
            newBinding = new Binding(new Literal(clause.literals.get(0)), true);
          else
            generatedBindings.add(new Binding(new Literal(clause.literals.get(0)), true));
        }
      }

      if (newBinding == null) return;
    }

    // add the new binding to the binding tracker (only if we are actively tracking this binding)
    if (bindings != null) {
      if (bindings.bindings.contains(newBinding))
        return;
      else if (bindings.bindings.contains(newBinding.opposite()))
        throw new IllegalEmptyClauseException("caused by: " + newBinding);
      bindings.bindings.add(newBinding);
    }

    // apply to every clause in this formula
    Iterator<Clause> clauseItr = clauses.iterator();
    while (clauseItr.hasNext()) {
      clause = clauseItr.next();
      removed = false;

      // apply to clause by checking binding against each literal in clause
      Iterator<Literal> literalItr = clause.literals.iterator();
      while (literalItr.hasNext() && !removed) {
        literal = literalItr.next();
        int comp = literal.compareTo(newBinding.literal);
        if (comp == 1) // different literals, no action
          continue;
        else if (comp == 0 && newBinding.binding || comp == -1 && !newBinding.binding) {
          // identical literals, satisfy the clause
          clauseItr.remove();
          removed = true;
        }
        else {
          // opposite literals, remove the literal
          literalItr.remove();
        }
      }

      // if the clause now contains 1 literal, generate a binding
      if (!removed && (failOnEmptySoftClause || clause.weight == Double.POSITIVE_INFINITY)) {
        if (clause.literals.size() == 0) {
          throw new IllegalEmptyClauseException("caused by: " + newBinding);
        }
        else if (clause.literals.size() == 1) {
          // propagate the new binding
          Binding generated = new Binding(new Literal(clause.literals.get(0)), true);
          generatedBindings.add(generated);
        }
      }
    }
    // repeat for new bindings
    for (Binding b : generatedBindings) {
      // failOnEmptySoftClause);
      propagate(b, bindings, failOnEmptySoftClause);
    }
  }

  /**
   * Selects a literal to bind using the heuristic given in section 3.3 of the paper: Let hard(l) be
   * number of occurrences of l in hard clauses Let soft(l) be sum of the weights of soft clauses
   * containing l Let meanWeight be mean weight among soft clauses Let score(l) = 2 * meanWeight *
   * hard(l) + soft(l) Select the literal with the highest value of: score(x) * score(!x) *
   * meanWeight + score(x) + score(!x)
   * 
   * @return selected literal
   */
  public Literal select()
  {
    // use maps to count data for each literal so we only have to iterate over the clauses once
    Map<Literal, Integer> hardCount = new HashMap<Literal, Integer>();
    Map<Literal, Double> softWeight = new HashMap<Literal, Double>();

    // use a set to track unique literals so we avoid calculating score for x and !x
    Set<Literal> uniqueLiterals = new HashSet<Literal>();

    // variables to track mean weight and best score
    double totalSoftWeight = 0;
    int softCount = 0;
    double bestScore = Double.NEGATIVE_INFINITY;
    Literal bestLiteral = null;

    // iterate through literals and do calculations
    for (Clause c : clauses) {
      // update variables to get mean weight for soft clauses
      if (!c.isHard()) {
        totalSoftWeight += c.weight;
        softCount++;
      }
      for (Literal literal : c.literals) {
        // make sure we have this literal in the literal set
        uniqueLiterals.add(literal.nonNegated());

        // for a hard clause just update the count
        if (c.isHard()) {
          Integer oldCount = hardCount.get(literal);
          hardCount.put(literal, (oldCount == null) ? 1 : ++oldCount);
        }
        // for a soft clause, update the total weight
        else {
          Double oldWeight = softWeight.get(literal);
          softWeight.put(literal, (oldWeight == null) ? c.weight : oldWeight + c.weight);
        }
      }
    }

    /*
     * set the best literal to something so that it doesn't come back null if all remaining clauses
     * are hard
     */
    bestLiteral = uniqueLiterals.iterator().next();

    double meanWeight = totalSoftWeight / softCount;
    double totalScore, scoreTrue, scoreFalse;
    Integer hardTrue, hardFalse;
    Double softTrue, softFalse;

    // calculate the total score for this literal
    for (Literal literal : uniqueLiterals) {
      // get hard(l) and hard(!l)
      hardTrue = hardCount.get(literal);
      if (hardTrue == null) hardTrue = 0;
      hardFalse = hardCount.get(literal.negated());
      if (hardFalse == null) hardFalse = 0;

      // get soft(l) and soft(!l)
      softTrue = softWeight.get(literal);
      if (softTrue == null) softTrue = 0.0;
      softFalse = softWeight.get(literal.negated());
      if (softFalse == null) softFalse = 0.0;

      // get scores
      scoreTrue = 2 * meanWeight * hardTrue + softTrue;
      scoreFalse = 2 * meanWeight * hardFalse + softFalse;
      totalScore = scoreTrue * scoreFalse * meanWeight + scoreTrue + scoreFalse;

      // track the best so far
      if (totalScore >= bestScore) {
        bestLiteral = literal;
        bestScore = totalScore;
      }
    }

    return bestLiteral;
  }

  /**
   * Estimates an upper bound of weight of the soft clauses that could be falsified if the current
   * partial assignment were extended to a complete assignment. This is done with the following
   * algorithm (3.3.2 from the paper): - build a graph G using the following rules: -- create a
   * vertex Vi for every undecided soft clause Ci -- add an edge between Vi and Vj if either: ---
   * there is some literal Lia and Ljb such that Lia = !Ljb --- the set of literals in Ci U Cj U
   * {hard clauses} is unsatisfiable by unit propagation - compute an incremental clique partition
   * of G by selecting V of minimum degree -- compute a max clique containing V -- let the clique's
   * weight = min weight of vertex in the clique -- decrement all clique members' weights by the
   * clique's weight and add this weight to the UB -- remove an members of weight 0 from the graph
   * -- repeat until the empty graph is derived
   * 
   * @return upper bound of weight of soft clauses that could be falsified
   */
  public double overestimate()
  {
    /*
     * We could build the graph by checking each pair of vertices to see if it needs an edge, but
     * this would cost O(literals^2) since each literal would be compared to every other literal. We
     * can do better by scanning the list once, placing vertices into buckets based on their literal
     * members and adding edges between vertices in conflicting buckets.
     */

    // only interested in nonempty soft clauses, but we need the hard clauses later
    List<Clause> undecidedClauses = new ArrayList<Clause>();
    List<Clause> hardClauses = new ArrayList<Clause>();
    for (Clause c : clauses)
      if (c.isHard())
        hardClauses.add(new Clause(c));
      else if (!c.literals.isEmpty()) undecidedClauses.add(new Clause(c));

    // use a set to track unique literals
    Set<Literal> uniqueLiterals = new HashSet<Literal>();
    Map<Literal, List<Integer>> presenceMap = new HashMap<Literal, List<Integer>>();

    // create the initial graph, 1 node per undecided clause
    Graph graph = new Graph(undecidedClauses.size());

    // iterate over the undecided soft clauses
    Clause c;
    for (int i = 0; i < undecidedClauses.size(); i++) {
      c = undecidedClauses.get(i);
      graph.addVertex(i, c.weight);
      for (Literal literal : c.literals) {
        uniqueLiterals.add(literal.nonNegated());
        createOrAppend(literal, i, presenceMap);
      }
    }

    // use the map to add edges
    List<Integer> trueVertices, falseVertices;
    for (Literal literal : uniqueLiterals) {
      // make sure there is at least 1 opposite relationship that gets an edge
      if ((trueVertices = presenceMap.get(literal)) != null
          && (falseVertices = presenceMap.get(literal.negated())) != null) {
        for (Integer i : trueVertices)
          for (Integer j : falseVertices)
            graph.addEdge(i, j);
      }
    }

    // bind unit soft clause to false (since its opposite is true) and propagate
    Binding unit;
    for (int i = 0; i < undecidedClauses.size(); i++) {
      c = new Clause(undecidedClauses.get(i));
      if (c.literals.size() == 1) { // unit clause eligible for propagation edges
        unit = new Binding(c.literals.get(0), false);
        for (int j = 0; j < undecidedClauses.size(); j++) {
          // if there is already an edge, no need to check propagation
          if (i != j && !graph.hasEdge(i, j)) {
            Formula toPropagate = new Formula();
            toPropagate.addClause(undecidedClauses.get(j).allLiteralsNegated());
            for (Clause hard : hardClauses)
              toPropagate.addClause(new Clause(hard));
            try {
              toPropagate.propagate(unit, null, true);
            }
            catch (IllegalEmptyClauseException e) {
              // this set is unsatisfiable, so add an edge
              graph.addEdge(i, j);
            }
          }
        }
      }
    }

    return graph.getUpperBound();
  }

  /**
   * Evaluates the current formula for the given mappings from non-negated literals to truth values
   * 
   * @param bindings
   *          Bindings from non-negated literals to truth values
   * @return Unsatisfied soft weight of the current assignment, or infinity if this assignment fails
   */
  public double evaluate(Map<String, Boolean> bindings)
  {
    double unsatSoftWeight = 0;

    Iterator<Clause> clauseItr = clauses.iterator();
    Clause c;
    Iterator<Literal> litItr;
    Literal lit;
    boolean removed;
    while (clauseItr.hasNext()) {
      c = clauseItr.next();
      removed = false;
      litItr = c.literals.iterator();
      while (litItr.hasNext() && !removed) {
        lit = litItr.next();
        Boolean binding = bindings.get(lit.name);
        if (binding == null)
          binding = true; // if nothing is bound then it means we don't care
        else if (binding && !lit.neg || !binding && lit.neg) { // satisfy the clause
          clauseItr.remove();
          removed = true;
        }
      }

      if (!removed) { // this clause is unsatisfied
        if (c.isHard())
          return Double.NEGATIVE_INFINITY;
        else
          unsatSoftWeight += c.weight;
      }
    }

    return unsatSoftWeight;
  }

  /**
   * Appends integer i to the list mapped by l in the map that is passed in, creating the list if it
   * does not yet exist
   */
  public static void createOrAppend(Literal l, Integer i, Map<Literal, List<Integer>> m)
  {
    List<Integer> intList;
    if ((intList = m.get(l)) == null) intList = new ArrayList<Integer>();
    intList.add(i);
    m.put(l, intList);
  }
}
